{"entities":{"Q2375421":{"pageid":2386164,"ns":120,"title":"Item:Q2375421","lastrevid":73761987,"modified":"2026-04-14T17:10:53Z","type":"item","id":"Q2375421","labels":{"en":{"language":"en","value":"The gauge integral theory in HOL4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6175744"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$C9268083-90E9-4847-9C71-88C2B0A454D1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"737aeeedc1273e185fbe005e357d90326c6cad28","datavalue":{"value":{"text":"The gauge integral theory in HOL4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2375421$CF723E6F-2D9C-474E-850E-04C64FDD890B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aac5f689a87fbe7398e6586e6ae7aee22c49b9da","datavalue":{"value":"1268.65033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$EE5806D9-CD29-486F-BDDE-A44F729926BC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ac1101e939221a261bb69dfed32718b71cfcd56f","datavalue":{"value":"10.1155/2013/160875","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$C70A290B-18CA-4B14-BEC8-8C29C62B548C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb41e43426ff3ff3f8a93f102f45b1fd00efc7eb","datavalue":{"value":{"entity-type":"item","numeric-id":826357,"id":"Q826357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$29D45827-C9DE-4390-9783-4A7428670366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"99d96a87a6ff1d72b2d8bbb042e3e666a10d98ae","datavalue":{"value":{"entity-type":"item","numeric-id":2375420,"id":"Q2375420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$BBE4430E-E956-47CE-9335-CC0E51F110AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a231db2bdce0e9b67cdf0dbd752c938210e47142","datavalue":{"value":{"entity-type":"item","numeric-id":471532,"id":"Q471532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$BF95663C-027F-43B5-8BF9-9D388F82A009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bad697f6be27ac07cc0bac5f2074dc40ed884baf","datavalue":{"value":{"entity-type":"item","numeric-id":258539,"id":"Q258539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$619DE50E-75A1-42B4-8CB7-1AE664A03260","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d0d64bff6a234e8e185575f6c485fb374ee059c","datavalue":{"value":{"entity-type":"item","numeric-id":2294127,"id":"Q2294127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$0B15534B-D626-456D-82C5-DFF28B2CB355","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d39b4536ab4b3691fa10e20a21c234518780f867","datavalue":{"value":{"entity-type":"item","numeric-id":1665985,"id":"Q1665985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$E3952095-A6C7-46CB-BC2E-8FCCF2FEC712","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ceeeb03fb5bd35f76f74e037e926f9b1ddfa2ff7","datavalue":{"value":{"entity-type":"item","numeric-id":1665986,"id":"Q1665986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$6E292F3E-5AFB-46F6-8435-6A55D3B51299","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$8E044EF6-608E-405B-8EA8-32959AD73D65","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b84d2a34981f1c1a0d0fb543ea5aabc14a21194b","datavalue":{"value":{"time":"+2013-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2375421$D1140873-01F3-4DBA-88DB-E1E0213E5C97","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"585d5fdcf4d4433d2d4bc8734df21481593a52ae","datavalue":{"value":"Summary: The integral is one of the most important foundations for modeling dynamical systems. The gauge integral is a generalization of the Riemann integral and the Lebesgue integral and applies to a much wider class of functions. In this paper, we formalize the operational properties which contain the linearity, monotonicity, integration by parts, the Cauchy-type integrability criterion, and other important theorems of the gauge integral in higher-order logic 4 (HOL4) and then use them to verify an inverting integrator. The formalized theorem library has been accepted by the HOL4 authority and will appear in HOL4 Kananaskis-9.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375421$5AE2B512-3B36-4C93-8E38-4C9F77C14665","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f167f1f4c1d109b89cd09b0dd6067acc1909209b","datavalue":{"value":"65D30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$244E03F1-A273-49EB-9D59-4E1EB57DCCC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"173ff65edcfc7a9a8461397b4283ab08ef6cd61e","datavalue":{"value":"26B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$F91AEF06-A153-4F11-B888-508A5A5B7B3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4844ecc2838b02f08a426d6ddfea94d07252b432","datavalue":{"value":"65Y15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$0C9F8AC1-4997-490D-B430-4449873D8A80","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"264b35933c80c5119d2e53f85420f82f78d2d55c","datavalue":{"value":"6175744","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$145CC5D9-E666-410F-833E-6C607D691741","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dad875ef6d2987fcdf1db17f24988889c0c3b306","datavalue":{"value":"gauge integral","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375421$F4A418EA-66B1-46E3-8562-EC0F1E2AD919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c11cbb7d24d51b747029ca5957b967934331ff1","datavalue":{"value":"Cauchy-type integrability criterion","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375421$81C4B4F0-7422-4345-AA40-1E132541936C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375421$E64BCE6B-9842-4EAD-A5F4-564E09AC232F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"47f111ce8e4c6fc25da9a8709686b31a918db4d7","datavalue":{"value":"HOL4 Kananaskis-9","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375421$5F10D140-BAAD-4CD8-B6E8-6C3A7C3015B1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$4E661D0F-2A0D-4268-968F-E2AE0D569091","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$F54A962D-B83E-4134-9808-24E43332B27B","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$99C69091-118A-42E3-AC5D-F789A810A89F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ec8c8893c7fab1d682c44a2ab7c28ed5925ba994","datavalue":{"value":"https://doi.org/10.1155/2013/160875","type":"string"},"datatype":"url"},"type":"statement","id":"Q2375421$60DB9AC9-5A50-4BFC-9499-7CCA27720C20","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9185ea38f2ec728b953d3634431c12f375ba8514","datavalue":{"value":"W2066086825","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$C90F0F01-3FFD-435E-A8E5-A7E677230D12","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"982fe7601c5d3423da83b2fd7f60f94b5ae36e70","datavalue":{"value":"Q59001913","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375421$2B67D438-D28F-4034-83AF-017A17120FAD","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc18b84f53cfdc559b4d296e04ba30186fce5df8","datavalue":{"value":{"entity-type":"item","numeric-id":5464655,"id":"Q5464655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$E5E25B94-A0E9-4A1F-B9C1-A2153BB8FBDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3738b03704797326830c6e1694271832e90c3c5","datavalue":{"value":{"entity-type":"item","numeric-id":2754041,"id":"Q2754041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$B2389666-336C-416D-A303-3BD173FA2A11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ff77ab8eae0071823dfece1650dbbf475b9f173","datavalue":{"value":{"entity-type":"item","numeric-id":3497626,"id":"Q3497626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$D7B7232D-0709-46C9-B018-3D00D103E3EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e1e49d74090d77a773896f7b2be0970d01b92ca","datavalue":{"value":{"entity-type":"item","numeric-id":5747663,"id":"Q5747663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$71BE678B-0AE3-495A-85AB-4A638BA4327C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$A7A32C0A-5311-40C0-84DA-93D9E0347642","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f154ed6511405fd4f83853438e2966ca3d49b409","datavalue":{"value":{"entity-type":"item","numeric-id":4490681,"id":"Q4490681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$4695AFE7-7B92-4302-A49A-017F7E8A96F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9fd10a5e643730e591a7fa3e0d5c9ab297cf80f6","datavalue":{"value":{"entity-type":"item","numeric-id":4307619,"id":"Q4307619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$50164FFD-0D0B-4B75-AD28-96C455326295","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"650a251a7e0571513452c98533ade9dfb3a7bce2","datavalue":{"value":{"entity-type":"item","numeric-id":1688749,"id":"Q1688749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b4ff2f51999d6e7ed498882bd9a5dc2641eeffb","datavalue":{"value":{"amount":"+0.8222070336341858","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2375421$A4B395A3-F220-4885-9E91-D675E14682DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"def5ac029f1cce2d8ece68002b014dbe2a9324db","datavalue":{"value":{"entity-type":"item","numeric-id":3015831,"id":"Q3015831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c58930e94ae56ac30525d46f1a661f863e5fb45","datavalue":{"value":{"amount":"+0.7392528057098389","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2375421$455EBB63-C7CD-42D2-9050-F81D9D2C7F2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f481d1562ef12fd442b7504ddc0be150ba4d26a6","datavalue":{"value":{"entity-type":"item","numeric-id":3088003,"id":"Q3088003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d035379b3e7b575e3f26453ac3d9359a9641dda","datavalue":{"value":{"amount":"+0.7242216467857361","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2375421$A43E0CF1-F918-4FC4-87F9-40711DBF2D70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e330724ed3cc9a5bc71103dc491805ab9103c50a","datavalue":{"value":{"entity-type":"item","numeric-id":987984,"id":"Q987984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0386e5495c3d2dc3dc8566c5649abb57b2db5464","datavalue":{"value":{"amount":"+0.7117647528648376","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2375421$50887F86-9E73-4F9B-94AE-B3250CC3794E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a642dd509fa39d333ce011f5fc7a90e147616c7e","datavalue":{"value":{"entity-type":"item","numeric-id":3497626,"id":"Q3497626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ed721127b681fac8dd51c5fd99a3b81238b36ad","datavalue":{"value":{"amount":"+0.7114678621292114","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2375421$ADD92C3E-97D6-427A-98C1-B8E91A2E3A1B","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375421$D966E9BB-CAA4-43C1-8827-C128AF5CEB27","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The gauge integral theory in HOL4","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_gauge_integral_theory_in_HOL4"}}}}}